X is finite
== finite-type({p::Id  Knd| e:E. (loc(e) = (p.1) & kind(e) = (p.2) & ((e  X)))} ) 

latex

---

clarification:

es-interface-finite(es;A;X)
== finite-type({p::Id  Knd| 
== finite-type({e:es-E(es)
== finite-type({(es-loc(es; e) = (p.1)  Id & es-kind(es; e) = (p.2)  Knd & ((e  X)))} ) 

latex

Definitions	finite-type(T), {x:A| B(x)} , x:A  B(x), x:A. B(x), E, Id, loc(e), t.1, P & Q, s = t, Knd, kind(e), t.2, b, e  X
FDL editor aliases	es-interface-finite